the_w:World, e:E.
FairFifo  (isrcv(kind(e)))  (index(e)  {0..||sends(lnk(kind(e));sender(e))||}) 

latex

Definitions	t  T, x:A. B(x), kind(e), isrcv(k), b, x:AB(x), {i..j}, P  Q, FairFifo, E, World, x:A  B(x), P & Q, A  B, i  j < k, {x:A| B(x)} , , {T}, time(e), lnk(k), match(l;t;t'), x.A(x), #$n, x:A. B(x), False, A, , sender(e), sends(l;e), index(e), mu(f), s = t, snds(l;t), Msg, ||as||, rcvs(l;t), destination(l), Action(i), n - m, -n, n+m, a < b, True, T, Void, P  Q
Lemmas	assert-w-match, w-action wf, ldst wf, w-rcvs wf, length wf1, w-Msg wf, w-snds wf, mu wf, w-match-exists, mu-property, nat wf, le wf, w-match wf, lnk wf, w-time wf, world wf, w-E wf, fair-fifo wf, assert wf, isrcv wf, w-ekind wf